namer-disjoint(n1;n2;nmr1;nmr2) == i:{0..n1}, j:{0..n2}. (nmr1(i) = nmr2(j)) 

latex

---

clarification:

namer-disjoint(n1;n2;nmr1;nmr2) == i:{0..n1}, j:{0..n2}. (nmr1(i) = nmr2(j)  Id) 

latex

Definitions	x:A. B(x), {i..j}, #$n, A, s = t, Id, f(a)
FDL editor aliases	namer-disjoint